00100 E(T(B B) D); 00200 E(T(C C) G); 00300 E(T(A G) D); 00400 D(X1 B) → ¬D(X1 C); 00500 ∀(X1 X2)∃(X3)(D(X1 X2) →E(T(X1 X3) X2)); 00600 D(X1 T(X1 X2)); 00700 (P(X1) ∧ D(X1 T(X2 X2)))→D(X1 X2); 00800 E(T(X1 T(X2 X3)) T(T(X1 X2) X3)); 00900 E(T(X1 X2) T(X2 X1)); 01000 (D(X1 X2) ∧ D(X2 X3)) →D(X1 X3);; 01100 ; 01200 ¬P(A);;